perm filename USER[245,JMC] blob
sn#002382 filedate 1970-06-19 generic text, type T, neo UTF8
00100 USING THE THEOREM-PROVER
00200
00300 John Allen and David Luckham
00400
00500 This is a short and rather rough guide to some of the little tricks
00600 involved in running the on-line theorem-prover. This program is not
00700 yet in a form suitable for general use. But (under some duress) this
00800 guide has been written so that the casual user can solve problems
00900 with it, even in its present incomplete state. A version suitable
01000 for general distribution should be ready in September 1970.
01100 Meantime, the user is advised to watch this space [245,JMC] USER -
01200 for updates and to acquaint himself with some of the theory (which is
01300 not explained here). Preferably, he should read A.I. Memos 103 and
01400 81; a more comprehensive bibliography of the literature is available
01500 on file [245,JMC] BIBLE.
01600
01700
01800
01900 CONTENTS
02000
02100 1. INPUT
02200
02300 2. FINDING THE PROVER, SETTING THE STRATEGIES, STARTING A PROOF.
02400
02500 3. STOPPING THE PROVER, LOOKING AT WHAT IT HAS DONE, CHANGING ITS
02600 MIND.
02700
02800 4. GETTING PRINTED OUTPUT.
02900
03000 5. DEFEATING THE SYSTEM.
03100
03200
03400 l. INPUT
03500
03600 The Prover accepts sets of clauses as input.
03700
03800 Identifiers are strings of characters not containing the negation
03900 symbol, ¬, nor the usual LISP delimiters.
04000
04100 SYNTAX:
04200
04300 <variable>::= x <numeral>
04350 <function symbol>::= <identifier>
04400 <predicate symbol>::= <identifier>
04500
04600 <term>::= <variable>|<function symbol>| <function symbol>(<argument
04700 string>)
04800
04900 <argument string>::= <term>|<term>,<argument string>
05000
05100 <atom>::= <predicate symbol>(<argument string>)
05200
05300 <literal>::= <atom>|¬<atom>
05400
05500 <clause>::= <literal>;|<literal><blank><clause> |<literal><carriage
05600 return><clause>
05700
05800 <clause list>::= <clause><blank>;|<clause><carriage return>;
05900 |<clause><clause list>
06000
06100 COMMENTS
06200
06300 1. The Prover will behave correctly only on those sets of clauses
06400 that satisfy: if a given function symbol has more than one
06500 occurrence, all such occurrences are followed by argument strings of
06600 equal length; similarly for occurrences of Predicate Symbols.
06700
06800 2. The Prover will accept clause lists either from the disk or from
06900 the console. It is probably safer to create a disk file containing
07000 the clause list before calling the Prover.
07400
07500 2. STARTING THE PROVER
07600
07700 2.1 Where to find the Prover:
07800
07900 The current compiled hopefully working version will be found on the
08000 disk file: [245,JMC] PROVER.
08100
08200 System command,
08300
08400 RUN DSK [245,JMC] PROVER
08500
08600 will call a 34k core memory image of the current LISP system, the
08700 Prover and enough working space to deal with many standard problems.
08800 The Prover replies,
08900
09000 *
09100
09200 at which point the user can set up the strategy combination for his
09300 problem.
09400
09500 If more core store working space is required, use:
09600
09700 1. RUN DSK [245,JMC] PROVER n
09800
09900 2. *
10000
10100 3. (CDR(QUOTE ACHLOC))
10200
10300 4. (sym number(pname....$
10400
10500 5. ↑C
10600
10700 6. .E number
10800
10900 7. 240040_777776
11000
11100 8. DE 402000_1_number
11200
11300 9. REE
11400
11500 10. *
11600
11700 Lines 1-10 will allot all extra storage to the free storage list. If
11800 extra full-word space is also required, simply omit lines 3, 4, 6, 7,
11900 8.
07450
12000 2.2 Setting the Strategies
12100
12200 The strategies are discussed in AIM-103 and other references.
12300 Having called the Prover, a suggested sequence for setting
12400 the strategy combination is as follows:
12500
12600 (QUERY T) Gives the current strategy settings.
12700 (QUERY NIL) Displays each (optional) strategy for user
12800 decision (below m and n are numerals):
12900
13000 STRATEGY USER REPLY EFFECT
13100
13200 SUPPORT = NIL NO SUPPORT
13300 n Axioms n, n+1,...,m
13400 form the Set of Support.
13500
13600 UNIT-PREFERENCE NIL No UNIT-PREFERENCE.
13700 n Unit-preference to a
13800 maximum depth of n+
13900 current level.
14000
14100 MERGE NIL No Merging
14200 T Merging
14300
14400 ORDER NIL No ordering strategy.
14500 T See AIM-103
14600
14700 ANCESTRY NIL NO AFF.
14800 T Restricts proof-trees
14900 to AFF.
15000
15100 DEPTH-BOUND m
15200
15300 LENGTH-BOUND n
15400
15500 DEBUG = NIL
15600 T Displays deductions on
15700 the Console.
15800
15900 MODEL = NIL
16000 T
16100
16200 if the reply was T,
16300
16400 POSITIVE-MODEL = (LISTL1 of Predicate Symbols) or NIL
16500 NEGATIVE-MODEL = (....L2 ) or NIL
16600 with proviso that L↓1∩L↓2 = 0.
16700
16800 PARAMODULATE = NIL
16900 T
17000
17100 If the reply was T,
17200
17300 EQUALITY - SYMBOL = Predicate Symbol
17400 PARA-DEPTH BOUND = n
17500 DEMODULATION LIST = clause list satisfying input format
17600 and conditions described in AIM-103.
17700
17800 2.3 Starting a Proof:
17900
18000 Having set the strategy combination the user is ready to
18100 start his problem. We recommend:
18200
18300 1. (NOUUO NIL) handles function calls faster
18400 2. T
18500 3. (PROVE DSK:<blank><file name>) starts the prover on
18600 the problem in the file.
18700 or
18800 (PROVE NIL) accepts the problem clause list
18900 from the console.
19000
19100 COMMENTS
19200
19300 1. Note that the file name in a call to the Prover MUST
19400 be preceded by a blank.
19500
19600 2. If DEBUG is set to T, the Prover will display the
19700 deductions on the scope as they are added to the clause
19800 list; those deductions eliminated by EDIT are not displayed.
19900 The current length of the clause list is also given. Each
20000 time a level is saturated the user is told and given a
20100 total count of clauses generated (independent of the value
20200 of DEBUG).
20300
20400 3. The Prover will STOP by itself under three conditions:
20500
20600 (i) A proof is found - this will be displayed on the scope.
20700 (ii) No further deductions are possible - comment "NOPROOF"
20800 is given.
20900 (iii) Out of Free-Storage or Full-Word space.
21000
21050
21100 3. STOPPING THE PROVER, LOOKING AT WHAT ITS DONE, CHANGING
21200 ITS MIND.
21300
21400 Press any key. This will stop the Prover in a subroutine
21500 called UPDATE. It will print out the first clause on the
21600 clause list and wait for user commands. Essentially the user
21700 can then run a pointer up and down the clause list displaying
21800 clauses, deleting and adding clauses, displaying proof trees of
21900 clauses, and computing resolvents and paramodulants. When update
22000 is ready for the next command it types * . The update commands
22100 followed by a carriage return or altmode have the following
22200 actions:
22300
22400 UPDATE COMMAND ACTION
22500
22600 F∨ displays members of the clause list, in
22700 order (down), in rapid sequence; stop
22800 by pressing a key. (here ∨ is the "or" key).
22900
23000 F∧ displays clauselist in reverse (up).
23050 (∧ is the "and" key).
23100
23200 nv moves n clauses down the list.
23300
23400 n∧ moves n clauses up the list.
23500
23600 v displays next clause down.
23700
23800 ∧ displays next clause up.
23900
24000 0∨ moves to last clause in list.
24100
24200 0∧ moves to first clause in list.
24300
24400 A displays the proof of the clause pointed
24500 at. (A for ancestry).
24600
24700 D deletes clause pointed at.
24800
24900 I inserts a list of clauses (format of
25000 section 1) typed from the console,
25100 at the end of the clause list.
25200
25300 E Enters EVAL LOOP
25400
25500 END EXITS from EVAL LOOP to UPDATE
25600
25700 T EXITS from UPDATE to PROVER. T for terminate.
25800
25900 The following commands use two extra points:
26000
26100 n: Set a pointer at clause n in the
26200 clause list.
26300
26400 : Sets a pointer to the clause
26500 pointed at.
26600
26700 _: Reset pointers to zero.
26800
26900 R If the pointers are set at m and n,
27000 this displays the resolvents of the
27100 mth and nth clauses.
27200
27300 P Displays paramodulants of mth and nth
27400 clauses.
27500
27600 S Appends resolvents to clause list. (S for save).
27700
27800 The E command enters a READ-EVAL loop. In this mode it is
27900 possible to execute any LISP computation. Of course, one
28000 runs the risk of clobbering the state of the Prover's
28100 computation. Some useful applications of the E command are
28200 as follows:
28300
28400 (i) Quiz Program Variables:
28500
28600 LVL gives the current level the Prover is working
28700 at.
28800
28900 Count gives the total number of clauses generated
29000 so far.
29100
29200 (length clauses) gives total number of clauses retained.
29300
29400 (real-lngth clauses) gives total number of active
29500 clauses so far.
29600
29700 (ii) Reset Strategies:
29800
29900 (Query T) reminds the user of the current setting.
30000
30100 The user may then reset any of the strategies and bounds
30200 by executing the appropriate SETQ or by patiently going through
30300 (Query Nil) again.
30400
30500 (iii) Initiate Sub-proofs:
30600
30700 More will be written here later.
30800
30850
30900 4. GETTING PRINTED OUTPUT
31000
31100 The following sort of sequence is generally used within
31200 the READ-EVAL LOOP after an E command to UPDATE, or
31300 else when the Prover's computation has stopped with a proof.
31400
31500 l) ↑C
31600 2) .A LPT.........until favorable reply.
31700 3) CONT
31800 4) *
31900 5) (OUTC(OUTPUT LPT:)T) will transfer all output to the
32000 line printer.
32100 6) Any information that would normally appear on the console
32200 can now be placed on the LPT; heavy use is made of the
32300 following:
32400
32500 (QUERY T) prints strategy setting.
32600 (PROOF LHP RHP) prints the proof if one has been found.
32700 (CLAUSES CLAUSES) prints the full clause list.
32800
32900 7) (OUTC NIL T) clears the buffer and delivers EoF.
33000 8) ↑C
33100 9) .D LPT Essential
33200 l0) CONT
33300
33400 If there is a large amount of output, it is quicker to use
33500 the disk:
33600
33700 l) (OUTC(OUTPUT DSK:<blank><filename>)T)
33800 -------------OUTPUT COMMANDS--------
33900
34000 2) (OUTC NIL T)
34100
34200 and then print <filename> on the LPT.
34300
34400 5. DEFEATING THE SYSTEM
34500
34600 It is possible to restart a Prover computation from a core
34700 memory image by using a function called (at the moment)
34800 ANCES1. This enables the user to guard to some extent against
34900 the all too frequent system crashes. The usual operating
35000 sequence is:
35100
35200 1) ↑C stop the prover
35300 2) SAVE DSK filename
35400 3) CONT continue computation.
35500 System failure
35600 4) RUN DSK filename when the system is restored.
35700 *
35800 5) (ANCES1 CLAUSES) This starts up the Prover where it left
35900 off in the basic cycle (AIM-103). Any
36000 UPDATE situation will be lost, but this
36100 is unimportant; computation between
36200 line 3 and the system failure will be
36300 repeated.
36400
36500 If the Prover runs out of working space it is also possible
36600 to expand this and continue:
36700
36800 1) ↑C
36900 2) CORE n
37000 3) .REE